Skip to content

fix: reach did not terminate on nightly, and depth alone was never going to bound it - #30

Merged
sotashimozono merged 2 commits into
mainfrom
fix/reach-must-terminate
Sep 9, 2026
Merged

fix: reach did not terminate on nightly, and depth alone was never going to bound it#30
sotashimozono merged 2 commits into
mainfrom
fix/reach-must-terminate

Conversation

@sotashimozono

Copy link
Copy Markdown
Member

My own regression, and how it reached main is part of the report.

#29 removed a MethodError that reach threw on sum(f(x) for x in xs). That throw was also,
accidentally, a terminator. Without it, on 1.14.0-DEV:

reach(f, Tuple{Vector{Float64}})   # [f(x) for x in xs]   — did not return
reach(g, Tuple{Vector{Float64}})   # sum(map(f, xs))      — did not return

Both answer in milliseconds on 1.12.2.

The nightly leg is continue-on-error, so it could not block the merge. I then cancelled the run
that had been sitting in runtest for 40 minutes, and a background job merged #29 the moment
gh pr checks reported nothing pending. The hang was on main for about forty minutes.

The fix, and why the existing bound was not one

maxdepth bounds how far the walk goes, not how much of it there is. Thirty-two levels branching
by sixteen candidates is not a finite amount of work in any useful sense, and visited only prunes
signatures that repeat — a higher-order call generates new ones.

The walk now carries a maxwork budget, shared with every subwalk, and spends :unknown with
why = :budget when it runs out.

Shared rather than per-branch, and the distinction is load-bearing: visited is deliberately reset
in _subwalk so a candidate reached under another branch is still walked here — which means
visited cannot also be the thing that bounds the total.

maxwork is a keyword on reach, reach(::Module) and reach_script, with the measurement in
the docstring. An entry point that comes back :unknown with a :budget in unresolved is a
different situation from one that is genuinely dynamic, and only the caller can decide to pay more.

The spec now pins what does not move

The verdict does move: [unstable(x) for x in xs] is :depends on 1.12.2 and :unknown on
1.14.0-DEV, because the budget runs out there first. :unknown is weaker; :clean would be false.

So the assertions are:

claim why it holds everywhere
every shape returns one of the three verdicts a throw is not a fourth verdict and neither is a hang
a caller that can reach a mark is never :clean the safety property the file exists to defend
the same shapes with nothing marked are :clean control — otherwise an analysis that never says :clean passes
maxwork = 1 gives :unknown with why === :budget the knob is reachable and says which bound it hit

Measured on both: 1237 assertions on 1.12.2, 1236 on 1.14.0-DEV, 190 behaviours, green.

🤖 Generated with Claude Code

…ing to bound it

My own regression, and the way it reached main is worth writing down. #29 removed a `MethodError`
that `reach` threw on `sum(f(x) for x in xs)`. That throw was also, accidentally, a terminator.
Without it, on 1.14.0-DEV:

    reach(f, Tuple{Vector{Float64}})   # [f(x) for x in xs]   — did not return
    reach(g, Tuple{Vector{Float64}})   # sum(map(f, xs))      — did not return

Both answer in milliseconds on 1.12.2. The nightly leg is `continue-on-error`, so it could not
block the merge; I then cancelled the run that was sitting in `runtest` and a background job
merged #29 the moment `gh pr checks` reported nothing pending. The hang was on main for about
forty minutes.

`maxdepth` bounds how FAR the walk goes, not how much of it there is. Thirty-two levels branching
by sixteen candidates is not a finite amount of work in any useful sense, and `visited` only prunes
signatures that repeat — a higher-order call generates new ones. So the walk now also carries a
`maxwork` budget, shared with every subwalk, and spends `:unknown` with `why = :budget` when it
runs out. That is what `:unknown` is for; the alternative was a call that never comes back.

Shared, not per-branch, and the distinction is load-bearing: `visited` is deliberately reset in
`_subwalk` so a candidate reached under another branch is still walked here, which means `visited`
cannot also be the thing that bounds the total.

`maxwork` is a keyword on `reach`, `reach(::Module)` and `reach_script`, with the measurement in
the docstring — a caller whose entry point comes back `:unknown` with a `:budget` is in a
different situation from one that is genuinely dynamic, and only they can decide to pay for more.

The spec now pins the property that does not move between versions, because the verdict does:
`[unstable(x) for x in xs]` is `:depends` on 1.12.2 and `:unknown` on 1.14.0-DEV. What must hold
everywhere is that a caller which can reach a mark is never reported `:clean` — with a control
that the same shapes with nothing marked behind them still are, so the assertion is not satisfied
by an analysis that never says `:clean` at all.

Measured on both: 1237 assertions on 1.12.2, 1236 on 1.14.0-DEV, 190 behaviours, green.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@github-actions github-actions Bot added the bug Something isn't working label Sep 9, 2026
@github-actions

github-actions Bot commented Sep 9, 2026

Copy link
Copy Markdown
Contributor

📚 Docs preview: https://codes.sota-shimozono.com/ExperimentalAPI.jl/previews/PR30/

(updates on each push to this PR)

@codecov

codecov Bot commented Sep 9, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

…ys so

Measured while answering "what happens with several marks behind one loop": budgets between "too
small to reach any" and the default report `:depends` with one, two, … of twelve found and the
rest never walked to. The verdict is right either way; the LIST is not complete, and
`truncated = true` is the only thing that says so.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@sotashimozono
sotashimozono merged commit 8b51f9c into main Sep 9, 2026
14 checks passed
@sotashimozono
sotashimozono deleted the fix/reach-must-terminate branch September 9, 2026 06:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant